/*
 * Configuration.h
 *
 *  Created on: Apr 30, 2012
 *      Author: kobe
 *
 * Configuration is a result of an application of rules to previous configuration.
 * Each configuration contains a list of sequent. Just like a line in the proof tree.
 */

#ifndef CONFIGURATION_H_
#define CONFIGURATION_H_

#include <vector>
#include "Sequent.h"
#include "Rule.h"
#include "VariousRule.h"
#include "AId.h"
#include "ATopR.h"
#include "ABottomL.h"
#include <string>
#include "Axiom.h"

class Configuration {
public:
	Configuration(Sequent*, std::vector<Rule*>*);
	virtual ~Configuration();
	bool prove();
	std::string toLatex();
	void setParent(Configuration*);
	Sequent* getSequent();
	Configuration* getParent();
private:
	Sequent*	mSequent;
	Configuration* mParent;
	Rule*	mRule;
	std::vector<Rule*>* mAvailableRule;
	std::vector<Configuration*>* mSubConfiguration;
	bool mIsProofTreeLeaf;
	Axiom* mAxiom;
	bool checkLoop(Sequent*);
};

#endif /* CONFIGURATION_H_ */
